open util/boolean

sig Cittadino {}

sig Referendum{
partecipazioni: some PartecipazRef,
favorevoli: some VotoReferendum,
contrari: some VotoReferendum,
promotori: some Cittadino,
liked: Bool,
esito: Bool}

sig PartecipazRef{
cittadino: one Cittadino}

sig VotoReferendum{
esito: Bool}


fact NessunCittadinoVotaPiuVolteIReferendum{
no disjoint r1, r2: PartecipazRef | r1.cittadino = r2.cittadino }

fact NessunaPartecipazioneFuoriDalReferendum{
all p: PartecipazRef | p in Referendum.partecipazioni}

fact StessoNumeroVotiEPartecipazioniReferendum{
all r:Referendum| #r.partecipazioni = #r.contrari + #r.favorevoli}

fact ReferendumLiked {
all r: Referendum| (#r.promotori>=2 implies r.liked=True) &&
							  (#r.promotori<  2 implies r.liked=False)}

fact NessunReferendumNonLikedVieneVotato{
all r:Referendum| r.liked=False implies (#r.partecipazioni=0 && r.esito=False &&
																 #r.favorevoli =0 && #r.contrari =0 )}

fact NessunVotoFuoriDalReferendum{
all v:VotoReferendum| all r:Referendum| v in r.favorevoli || v in r.contrari}

fact NessunVotoSiaInFavorevoliCheInContrari{
no v:VotoReferendum| v in Referendum.favorevoli && v in Referendum.contrari}

fact TuttiIVotiInFavorevoliSonoTrue{
all v: Referendum.favorevoli| v.esito=True}

fact TuttiIVotiInContrariSonoFalse{
all v:Referendum.contrari| v.esito=False}

fact EsitoReferendum{
all r:Referendum| (#r.favorevoli>  #r.contrari) implies r.esito=True}

pred show()
{
#Cittadino=6
#Referendum=1
#Referendum.favorevoli=3
#Referendum.contrari=2

}
run show for 6
